#pragma once

/**********************************************************
oxsat - portable sat solver for windows and unix
Copyright (C) 2017  tj bandrowsky

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
*/

#include "variable.h"

namespace solver
{
	class literal
	{
	public:
		variable_reference ref;
		variable_value  val;
		variable_reference parent;

		literal() : val(0), ref(0), parent(-1)
		{
			;
		}

		literal(const literal& lit) : ref(lit.ref), val(lit.val), parent(lit.parent)
		{

		}

		literal(const literal&& lit) : ref(lit.ref), val(lit.val), parent(lit.parent)
		{

		}

		literal(variable_reference xref, variable_value xspin) : ref(xref), val(xspin), parent(-1)
		{

		}

		literal(variable_reference xref) : ref(xref), val(0), parent(-1)
		{

		}

		literal &operator = (const literal& lit) 
		{
			ref = lit.ref;
			val = lit.val;
			return *this;
		}

		bool matches_ref(const literal& b) const
		{
			return ref == b.ref;
		}

		bool operator == (const literal& b) const
		{
			return ref == b.ref && val == b.val;
		}

		bool operator != (const literal &b) const
		{
			return !(*this == b);
		}

		bool operator < (const literal &b) const
		{
			return ref < b.ref || val < b.val;
		}

		bool operator > (const literal &b) const
		{
			return ref > b.ref || val > b.val;
		}

	};

	class literal_compare_type
	{
	public:
		inline static int compare(literal& a, literal& b)
		{
			int c0 = a.ref - b.ref;
			if (!c0) c0 = a.val - b.val;
			return c0;
		}
	};


	typedef literal* pliteral;
}
